//---------DATA TYPE-------//------------SIGNATURE----------//
sig Integer{}
sig Strings{}
sig Location{
	street: one Strings,
	number: one Integer,
	zipCode: one Integer,
	city: one Strings,
	nation: one Strings
}

sig Icon{
	path: one Strings
}

sig WeatherForecast{
	type: one Strings,
	icon: one Icon
}

//---------ABSTRACT ENTITY-------//------------SIGNATURE----------//

//abstract class of calendar
abstract sig Calendar{
	owner: one RegisteredUser,
	publicEvent: set PublicEvent,
	privateEvent: set PrivateEvent
}

//abstract class of user
abstract sig User{}

//abstract class of event
abstract sig Event{
	owner: one RegisteredUser,
	title: one Strings,
	description: one Strings,
	date: one DateEvent,
	place: one Location,
	weatherForecast: lone WeatherForecast,
	invitedUser: some RegisteredUser
}

//abstract (generic date class)
abstract sig Date{
	year: one Integer,
	month: one Integer,
	day: one Integer,
}

//abstract calss of notify
abstract sig Notify{
	id: one Strings,
	message: one Strings
}

//---------DEFINITION OF ABSTRACT ENTITY-------//------------SIGNATURE----------//

//class notification

sig Notification{
	user: one RegisteredUser,
	notifyLink: some NotifyLink,
	notifyReply: some NotifyReply,
	notifyInfo: some NotifyInfo	
}

//visitor and registered user are disjoint
sig Visitor extends User{}

//user after registration
sig RegisteredUser extends User{
	name: one Strings,
	surname: one Strings,
	mail: one Strings,
	dateOfBirth: one DateBirth,
	address: one Strings,
	username: one Strings,
	password: one Strings,
}

//date for birth
sig DateBirth extends Date{}

//date  for the event
sig DateEvent extends Date{
	hour: one Integer,
	minutes: one Integer
}

//public event
sig PublicEvent extends Event{
	registeredUser: some RegisteredUser
}

//private event
sig PrivateEvent extends Event{}

//private calendar
sig PrivateCalendar extends Calendar{}

//public calendar
sig PublicCalendar extends Calendar{
	user: some RegisteredUser
}

//notify with link
sig NotifyLink extends Notify{
	link: one Strings
}

//notify with reply
sig NotifyReply extends Notify{
 reply: one Integer
}

//notify with information
sig NotifyInfo extends Notify{}

//---------FACTS-------//

//no empity date
fact noEmpityDate{
	all d : Date | (#d.year=1) and (#d.month=1) and (#d.day=1)
}

//no empity date for event
fact noEmpityDateEvent{
	all d : DateEvent | (#d.hour=1) and (#d.minutes=1)
}

//no empity location
fact noEmpityLocation{
	all l : Location | (#l.street=1) and (#l.number=1) and (#l.zipCode=1) and (#l.city=1) and (#l.nation=1)
}

//no empity calendar
fact noEmpityCalendar{
	all c : Calendar | (#c.owner=1)
}

//no empity event
fact noEmpityEvent{
	all e : Event | (#e.owner=1) and (#e.title=1) and (#e.description=1) and (#e.date=1) and (#e.place=1)
}

//no empity notify
fact noEmpityNotify{
	all n: Notify | (#n.message=1)
}

//no duplicate id notify
fact noDuplicateNotify{
	no disj n1, n2: Notify | n1.id=n2.id
}

//no duplicate user, impose no duplicate mail and no duplicate username
fact noDuplicateUser{
	no disj u1, u2: RegisteredUser | (u1.mail=u2.mail) and  (u1.username=u2.username)
}

//limit inviting User one time
fact noDoubleInvite{
	no disj u1,u2:RegisteredUser, e: PublicEvent | e.invitedUser=u1 and e.invitedUser=u2 and u1=u2
}

//impose no self invite to an event
fact noSelfInvite{
	all u: RegisteredUser, e: PublicEvent | not ((e.invitedUser=u) and (e.owner=u))
}

//---------ASSERT-------//


//no self invite to an event
assert noSelfInvites{
	no u: RegisteredUser, e: PublicEvent | (e.invitedUser=u) and (e.owner=u)
}
check noSelfInvites for 5

//check no double user invited to same event
assert noDoubleInvites{
	no disj u1,u2: RegisteredUser, e: PublicEvent |  e.invitedUser=u1 and e.invitedUser=u2 and u1=u2
}
check noDoubleInvites for 5

//check delete event pred
assert deleteEvent{
	all e: Event, c1, c2: Calendar | (e in c1.publicEvent) and deletePublicEvents[e,c1,c2] implies (e not in c2.publicEvent)
	all e: Event, c1, c2: Calendar | (e in c1.privateEvent) and deletePrivateEvents[e,c1,c2] implies (e not in c2.privateEvent)	
}
check deleteEvent

//check add event pred
assert addEvent{
	all e: Event, c1, c2: Calendar | (e not in c1.publicEvent) and addPublicEvents[e,c1,c2] implies (e in c2.publicEvent)
	all e: Event, c1, c2: Calendar | (e not in c1.privateEvent) and addPrivateEvents[e,c1,c2] implies (e in c2.privateEvent)	
}
check addEvent for 5

//check delete user pred
assert deleteUser{
	all u, u1, u2: RegisteredUser | (u in u1) and deleteUser[u, u1, u2] implies (u not in u2)
}
check deleteUser for 5

//check add user pred
assert addUser{
	all u, u1, u2: RegisteredUser | (u not in u1) and addUser[u, u1, u2] implies (u in u2)
}
check addUser for 5

//---------PREDICATES-------//

pred show(){
#RegisteredUser>1
#PublicEvent>1
#PrivateEvent>1
#NotifyInfo>1
}
run show for 30

//pred for add public event
pred addPublicEvents( e: PublicEvent, c1, c2: Calendar){
	e not in c1.publicEvent implies c2.publicEvent=c1.publicEvent+e
}
run addPublicEvents for 5

//pred for add private event
pred addPrivateEvents( e: PrivateEvent, c1, c2: Calendar){
	e not in c1.privateEvent implies c2.privateEvent=c1.privateEvent+e
}
run addPrivateEvents for 5

//pred for delete public event
pred deletePublicEvents( e: PublicEvent, c1, c2: Calendar){
	c2.publicEvent=c1.publicEvent-e
}
run deletePublicEvents for 5

//pred for delete private event
pred deletePrivateEvents( e: PrivateEvent, c1, c2: Calendar){
	c2.privateEvent=c1.privateEvent-e
}
run deletePrivateEvents for 5

//pred for add user
pred addUser( u,u1,u2: User){
	u not in u1 implies u2=u1+u
}
run addUser for 5

//pred for delete user
pred deleteUser( u,u1,u2: User){
	u in u1 implies u2=u1-u
}
run deleteUser for 5
